Add Erdős Problem 1173 (set mappings on ω_{ω+1} under GCH)#3794
Add Erdős Problem 1173 (set mappings on ω_{ω+1} under GCH)#3794henrykmichalewski wants to merge 5 commits into
Conversation
Mirrors the Round C docstring pass from the private repo's phase1-infrastructure branch. Each Lean file now carries the canonical source statement and upstream URL inline so reviewers can verify formalization against the source without navigating away from the diff.
| @@ -0,0 +1,196 @@ | |||
| /- | |||
| Copyright 2025 The Formal Conjectures Authors. | |||
There was a problem hiding this comment.
nit: Could you update the copyright year to 2026 for this new file?
|
|
||
| Here the domain is the type `(ω_ (ω + 1)).ToType` corresponding to the initial ordinal | ||
| $\omega_{\omega+1}$, and `Set (ω_ (ω + 1)).ToType` is the powerset. -/ | ||
| def IsSetMapping (f : (ω_ (ω + 1)).ToType → Set (ω_ (ω + 1)).ToType) : Prop := |
There was a problem hiding this comment.
Should a set mapping include the self-avoidance condition α ∉ f α? The source says set mapping, and the PR description mentions x ∉ f x, but IsSetMapping currently only has the size and almost-disjointness bounds. Could you add that condition to the predicate?
| **Monotonicity of `IsFreeSet`**: If $Y$ is a free set and $Z \subseteq Y$, then $Z$ is also free. | ||
|
|
||
| Free sets are downward-closed under inclusion. -/ | ||
| @[category undergraduate, AMS 3] |
There was a problem hiding this comment.
nit: Looks like this file still uses @[category undergraduate] for a few auxiliary/supporting lemmas. This now no longer works on main - the new version of this is textbook.
Paul-Lez
added
the
awaiting-author
…ook] + copyright 2026 Per Paul-Lez review on PR google-deepmind#3794. Mechanical nits applied on top of an upstream/main merge to pick up the new attribute infrastructure (google-deepmind#3900).
|
@Paul-Lez — applied the mechanical nits in |
…Paul-Lez review) Per Paul-Lez's review and the standard set-mapping definition (also mentioned in the original PR description), the predicate must include the self-avoidance condition `α ∉ f α`. Add it as the first conjunct of `IsSetMapping`, and update the supporting `image_lt_aleph_succ` lemma to project through the new conjunct order (`hf.2.1` instead of `hf.1`).
|
Thanks for the review @PaulLez. Pushed 0a34aed on |
2 participants
Formalizes Erdős Problem 1173 on set mappings and free sets on
ω_{ω+1}under GCH.Contents
IsSetMappingdefinition (a set mappingf : α → Set αwithx ∉ f xand a size bound).IsFreeSetdefinition (a subset pairwise disjoint from the mapping's images).IsSetMappingin the size boundCloses #1996
Assisted by Claude (Anthropic).